$\forall$$T$:Type, $f$:($T$$\rightarrow$$T$). retraction($T$;$f$) $\Rightarrow$ ($\forall$$x$, $y$, $z$:$T$. $y$ is $f$$\ast$($x$) $\Rightarrow$ $z$ = $f$+($y$) $\Rightarrow$ $z$ = $f$+($x$))